Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	active(from(X))	→ mark(cons(X,from(s(X))))
2:	active(first(0,Z))	→ mark(nil)
3:	active(first(s(X),cons(Y,Z)))	→ mark(cons(Y,first(X,Z)))
4:	active(sel(0,cons(X,Z)))	→ mark(X)
5:	active(sel(s(X),cons(Y,Z)))	→ mark(sel(X,Z))
6:	active(from(X))	→ from(active(X))
7:	active(cons(X1,X2))	→ cons(active(X1),X2)
8:	active(s(X))	→ s(active(X))
9:	active(first(X1,X2))	→ first(active(X1),X2)
10:	active(first(X1,X2))	→ first(X1,active(X2))
11:	active(sel(X1,X2))	→ sel(active(X1),X2)
12:	active(sel(X1,X2))	→ sel(X1,active(X2))
13:	from(mark(X))	→ mark(from(X))
14:	cons(mark(X1),X2)	→ mark(cons(X1,X2))
15:	s(mark(X))	→ mark(s(X))
16:	first(mark(X1),X2)	→ mark(first(X1,X2))
17:	first(X1,mark(X2))	→ mark(first(X1,X2))
18:	sel(mark(X1),X2)	→ mark(sel(X1,X2))
19:	sel(X1,mark(X2))	→ mark(sel(X1,X2))
20:	proper(from(X))	→ from(proper(X))
21:	proper(cons(X1,X2))	→ cons(proper(X1),proper(X2))
22:	proper(s(X))	→ s(proper(X))
23:	proper(first(X1,X2))	→ first(proper(X1),proper(X2))
24:	proper(0)	→ ok(0)
25:	proper(nil)	→ ok(nil)
26:	proper(sel(X1,X2))	→ sel(proper(X1),proper(X2))
27:	from(ok(X))	→ ok(from(X))
28:	cons(ok(X1),ok(X2))	→ ok(cons(X1,X2))
29:	s(ok(X))	→ ok(s(X))
30:	first(ok(X1),ok(X2))	→ ok(first(X1,X2))
31:	sel(ok(X1),ok(X2))	→ ok(sel(X1,X2))
32:	top(mark(X))	→ top(proper(X))
33:	top(ok(X))	→ top(active(X))

There are 49 dependency pairs:


34:	ACTIVE(from(X))	→ CONS(X,from(s(X)))
35:	ACTIVE(from(X))	→ FROM(s(X))
36:	ACTIVE(from(X))	→ S(X)
37:	ACTIVE(first(s(X),cons(Y,Z)))	→ CONS(Y,first(X,Z))
38:	ACTIVE(first(s(X),cons(Y,Z)))	→ FIRST(X,Z)
39:	ACTIVE(sel(s(X),cons(Y,Z)))	→ SEL(X,Z)
40:	ACTIVE(from(X))	→ FROM(active(X))
41:	ACTIVE(from(X))	→ ACTIVE(X)
42:	ACTIVE(cons(X1,X2))	→ CONS(active(X1),X2)
43:	ACTIVE(cons(X1,X2))	→ ACTIVE(X1)
44:	ACTIVE(s(X))	→ S(active(X))
45:	ACTIVE(s(X))	→ ACTIVE(X)
46:	ACTIVE(first(X1,X2))	→ FIRST(active(X1),X2)
47:	ACTIVE(first(X1,X2))	→ ACTIVE(X1)
48:	ACTIVE(first(X1,X2))	→ FIRST(X1,active(X2))
49:	ACTIVE(first(X1,X2))	→ ACTIVE(X2)
50:	ACTIVE(sel(X1,X2))	→ SEL(active(X1),X2)
51:	ACTIVE(sel(X1,X2))	→ ACTIVE(X1)
52:	ACTIVE(sel(X1,X2))	→ SEL(X1,active(X2))
53:	ACTIVE(sel(X1,X2))	→ ACTIVE(X2)
54:	FROM(mark(X))	→ FROM(X)
55:	CONS(mark(X1),X2)	→ CONS(X1,X2)
56:	S(mark(X))	→ S(X)
57:	FIRST(mark(X1),X2)	→ FIRST(X1,X2)
58:	FIRST(X1,mark(X2))	→ FIRST(X1,X2)
59:	SEL(mark(X1),X2)	→ SEL(X1,X2)
60:	SEL(X1,mark(X2))	→ SEL(X1,X2)
61:	PROPER(from(X))	→ FROM(proper(X))
62:	PROPER(from(X))	→ PROPER(X)
63:	PROPER(cons(X1,X2))	→ CONS(proper(X1),proper(X2))
64:	PROPER(cons(X1,X2))	→ PROPER(X1)
65:	PROPER(cons(X1,X2))	→ PROPER(X2)
66:	PROPER(s(X))	→ S(proper(X))
67:	PROPER(s(X))	→ PROPER(X)
68:	PROPER(first(X1,X2))	→ FIRST(proper(X1),proper(X2))
69:	PROPER(first(X1,X2))	→ PROPER(X1)
70:	PROPER(first(X1,X2))	→ PROPER(X2)
71:	PROPER(sel(X1,X2))	→ SEL(proper(X1),proper(X2))
72:	PROPER(sel(X1,X2))	→ PROPER(X1)
73:	PROPER(sel(X1,X2))	→ PROPER(X2)
74:	FROM(ok(X))	→ FROM(X)
75:	CONS(ok(X1),ok(X2))	→ CONS(X1,X2)
76:	S(ok(X))	→ S(X)
77:	FIRST(ok(X1),ok(X2))	→ FIRST(X1,X2)
78:	SEL(ok(X1),ok(X2))	→ SEL(X1,X2)
79:	TOP(mark(X))	→ TOP(proper(X))
80:	TOP(mark(X))	→ PROPER(X)
81:	TOP(ok(X))	→ TOP(active(X))
82:	TOP(ok(X))	→ ACTIVE(X)

The approximated dependency graph contains 8 SCCs: {55,75}, {57,58,77}, {54,74}, {56,76}, {59,60,78}, {62,64,65,67,69,70,72,73}, {41,43,45,47,49,51,53} and {79,81}.

Consider the SCC {55,75}. There are no usable rules. By taking the AF π with π(CONS) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 55 is weakly decreasing and rule 75 is strictly decreasing. There is one new SCC.
- Consider the SCC {55}. By taking the AF π with π(CONS) = 1 together with the lexicographic path order with empty precedence, rule 55 is strictly decreasing.

Consider the SCC {57,58,77}. There are no usable rules. By taking the AF π with π(FIRST) = π(mark) = 1 together with the lexicographic path order with empty precedence, the rules in {57,58} are weakly decreasing and rule 77 is strictly decreasing. There is one new SCC.
- Consider the SCC {57,58}. By taking the AF π with π(FIRST) = 1 together with the lexicographic path order with empty precedence, rule 58 is weakly decreasing and rule 57 is strictly decreasing. There is one new SCC.
  - Consider the SCC {58}. By taking the AF π with π(FIRST) = 2 together with the lexicographic path order with empty precedence, rule 58 is strictly decreasing.

Consider the SCC {54,74}. There are no usable rules. By taking the AF π with π(FROM) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 54 is weakly decreasing and rule 74 is strictly decreasing. There is one new SCC.
- Consider the SCC {54}. By taking the AF π with π(FROM) = 1 together with the lexicographic path order with empty precedence, rule 54 is strictly decreasing.

Consider the SCC {56,76}. There are no usable rules. By taking the AF π with π(mark) = π(S) = 1 together with the lexicographic path order with empty precedence, rule 56 is weakly decreasing and rule 76 is strictly decreasing. There is one new SCC.
- Consider the SCC {56}. By taking the AF π with π(S) = 1 together with the lexicographic path order with empty precedence, rule 56 is strictly decreasing.

Consider the SCC {59,60,78}. There are no usable rules. By taking the AF π with π(mark) = π(SEL) = 1 together with the lexicographic path order with empty precedence, the rules in {59,60} are weakly decreasing and rule 78 is strictly decreasing. There is one new SCC.
- Consider the SCC {59,60}. By taking the AF π with π(SEL) = 1 together with the lexicographic path order with empty precedence, rule 60 is weakly decreasing and rule 59 is strictly decreasing. There is one new SCC.
  - Consider the SCC {60}. By taking the AF π with π(SEL) = 2 together with the lexicographic path order with empty precedence, rule 60 is strictly decreasing.

Consider the SCC {62,64,65,67,69,70,72,73}. There are no usable rules. By taking the AF π with π(from) = π(PROPER) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {62,67} are weakly decreasing and the rules in {64,65,69,70,72,73} are strictly decreasing. There is one new SCC.
- Consider the SCC {62,67}. By taking the AF π with π(from) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 62 is weakly decreasing and rule 67 is strictly decreasing. There is one new SCC.
  - Consider the SCC {62}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 62 is strictly decreasing.

Consider the SCC {41,43,45,47,49,51,53}. There are no usable rules. By taking the AF π with π(ACTIVE) = π(cons) = π(from) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {41,43,45} are weakly decreasing and the rules in {47,49,51,53} are strictly decreasing. There is one new SCC.
- Consider the SCC {41,43,45}. By taking the AF π with π(ACTIVE) = π(cons) = π(from) = 1 together with the lexicographic path order with empty precedence, the rules in {41,43} are weakly decreasing and rule 45 is strictly decreasing. There is one new SCC.
  - Consider the SCC {41,43}. By taking the AF π with π(ACTIVE) = π(cons) = 1 together with the lexicographic path order with empty precedence, rule 43 is weakly decreasing and rule 41 is strictly decreasing. There is one new SCC.
    - Consider the SCC {43}. By taking the AF π with π(ACTIVE) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 43 is strictly decreasing.

Consider the SCC {79,81}. The usable rules are {1-31}. The constraints could not be solved.

Tyrolean Termination Tool (114.56 seconds) --- May 3, 2006